\section{Herbrandova veta}

\begin{lema}[Dirichletov princíp]
%%% {{{
    Nech $X,Y$ sú konečné množiny. Ak platí
    $|X| > |Y|$, potom pre každé zobrazenie
    $F:X \mapsto Y$ platí
    \begin{equation*}
        \exists y \in Y:
            \exists x_1,x_2 \in X:\ 
                [x_1 \ne x_2] \land [f(x_1)=y=f(x_2)]
    \end{equation*}
    Tvrdenie možno rozšíriť aj na prípad, že $X$ je nekonečná.
    Vtedy platí
    \begin{equation*}
        \exists y\in Y:
            \textit{množina }\{ x\in X: f(x)=y \}
            \textit{ je nekonečná}
    \end{equation*}
%%% }}}    
\end{lema}
\begin{dokaz}
%%% {{{
    Dôkaz sa robí sporom. V prvom prípade dostaneme, že ak tvrdenie
    neplatí, $f$ by mala byť injektívna, čo je ale spor s
    mohutnosťami. V druhom prípade $X$ vieme rozložiť na niekoľko
    tried ekvivalencie podľa hodnoty $f(x)$ a nutne aspoň jedna z nich
    musí byť nekonečná.
    \\
%%% }}}
\end{dokaz}

\begin{definicia}[Usporiadanie stromu]
%%% {{{
    Náš sémantický strom budeme chápať ako usporiadanú dvojicu 
    $(T,\le)$ kde $T$ je množina vrcholov a ``$\le$'' je relácia,
    ktorá čiastočne usporadúva $T$.
    Požadujeme, aby platilo

    \begin{enumerate}
	\item $T(u)=\{v\in T, v<u\}$ je dobre usporiadaná 
            (každá jej neprázdna podmnožina má najmenší prvok).

	\item $T$ má najmenší vrchol (koreň)
    \end{enumerate}

    Ak máme prvky $u,v$ a neexistuje $z$ také, že $u < z < v$,
    hovoríme, že prvok $v$ nasleduje bezprostredne po prvku $u$.
    %%% }}}
\end{definicia}

\begin{lema}[K\"onig] 
    Nech každý vrchol stromu s koreňom má konečné vetvenie
    (t.j. konečný stupeň vetvenia) a strom $T$ je nekonečný.
    Potom v ňom existuje nekonečne dlhá vetva.
\end{lema}

\begin{dokaz} 
%%% {{{
    Uvažujme strom $(T_1,\leq)$ a vrchol $v \in T$.
    Označme množinu tých vrcholov, ktoré ležia pod $v$, teda
    $A_v = \{ u \in T | v <u \}$.
    Nech $v_1, v_2, \dots, v_n$ sú bezprostrední nasledovníci vrchola $v$ (obr.
    \ref{fig:nasledovnici}). 
    \begin{figure}[h]
        \centering\includegraphics{img/10/nasledovnici.1.mps}
        \caption{Nasledovníci $v$}
        \label{fig:nasledovnici}
    \end{figure}
    Potom platí
    \begin{equation*}
        A_v = A_{v_1} \cup A_{v_2} \cup \ldots \cup A_{v_n}
        \cup \{v_1, v_2, \ldots, v_n\}
    \end{equation*}
    Predpokladáme, že $A_v$ je nekonečná.
    Na základe Dirichletovho princípu potom jedna z množín $A_{v_i}$
    musí byť nekonečná.

    Vybereme si $x_0$ ako koreň (najmenší vrchol stromu $T$). 
    $A_{x_0} = T \backslash \{x_0\}$ a teda $A_{x_0}$ je nekonečná.
    Teraz viem ale nájsť pre $x_0$ nasledovníka $x_1$, pre ktorý
    $A_{x_1}$ je nekonečné. A pre ten vieme nájsť nasledovníka $x_2$,
    pre $x_2$ vieme nájsť $x_3$ atď.
    Vieme teda zostrojiť nekonečnú postupnosť nasledovníkov koreňa a
    teda v strome existuje nekonečne dlhá cesta z koreňa.
%%% }}}    
\end{dokaz}

Po krátkej príprave sa môžeme pustiť do hlavnej časti, ktorá nás
zaujíma. Budeme si formulovať Herbrandovu vetu, tradične v dvoch
variantoch.

\begin{veta}[Herbrandova, 1. variant]
    Množina klauzúl $S$ nie je splniteľná práve vtedy,
    keď ľubovoľnému úplnému sémantickému stromu pre množinu klauzúl
    $S$ zodpovedá konečný uzavretý sémantický strom,
    t.j. ľubovoľná vetva úplného stromu vedie do odmietajúceho vrchola.
\end{veta}

\begin{dokaz}
%%% {{{
    \noindent
    \begin{itemize}
    \item[$\Rightarrow:$] Predpokladajme, že množina klauzúl $S$
        nie je splniteľná (nie je splniťeľná pre ľubovoľnú
        H-interpretáciu).
        Nech $T$ je úplný sémantický strom prislúchajúci množine $S$.
        Označme ako $I_V$ množina všetkých literálov
        pripísaných vetve $V$ stromu $T$.
        Potom $I_V$ možno chápať ako interpretáciu množiny klauzúl $S$.

        Predpokladajme, že $S$ je nesplniteľná
        (teda nesplniteľná v každej interpretácii).
        To znamená, že pre klauzulu $C$ existuje nejaká
        základná inštancia $C'$, ktorá je v interpretácii $I_V$ odmietnutá.

        Ešte potrebujeme zabezpečiť, aby strom bol konečný.
        To ale musí byť, lebo ak by existovala nekonečná vetva,
        bola by to interpretácia, ktorá by neodmietala žiadnu zo
        základných inštancií.

    \item[$\Leftarrow:$] Teraz predpokladáme,
        že k úplnému sémantickému stromu pre množinu klauzúl $S$
        existuje konečný uzavretý sémantický strom.
        Teda každá vetva stromu $T$ končí v zamietajúcom vrchole.
        Nuž ale potom evidentne musí byť $S$ odmietnutá v každej
        interpretácii a teda nie je splniteľná.
    \end{itemize}
%%% }}}
\end{dokaz}

\begin{veta}[Herbrandova, 2. variant]
    Množina klauzúl $S$ nie je splniteľná $\iff$
    existuje konečná podmnožina $S'$ základných inštancií klauzúl z $S$,
    ktorá nie je splniteľná.
\end{veta}

\begin{dokaz}
%%% {{{
    \noindent
    \begin{itemize}
    \item[$\Rightarrow:$] Predpokladajme, že množina klauzúl $S$
        nie je splniteľná. Na základe variantu 1 Herbrandovej vety
        platí, že ku každému úplnému sémantickému stromu $T$ pre
        množinu klauzúl $S$ existuje uzavretý konečný sémantický
        strom $T'$. Ak teraz zoberieme množinu základných inštancií
        klauzúl z $T'$, ktoré prislúchajú odmietajúcim vrcholom (čiže
        listom), dostávame konečnú množinu $S' \subseteq S$,
        ktorá tiež nie je splniteľná.

    \item[$\Leftarrow:$] Predpoklajme, že existuje
        konečná množina $S'$ základných inštancií klauzúl $S$,
        ktorá nie je splniteľná.
        Vezmime si $I$ interpretáciu $S$.
        Nech $I'$ je ``zúženie'' interpretácie $I$ na $S'$.
        Z nesplniteľnosťi $S'$ vyplýva, že $I'$ odmieta $S'$.

        Interpretácia $I$ obsahuje $I'$, teda keď $I'$ odmieta $S'$,
        potom $I$ odmieta $S$ a teda $S$ je nesplniteľná.
    \end{itemize}
%%% }}}
\end{dokaz}

\begin{priklad}
    Majme množinu klauzúl $S=\{P(x),\ \neg P(f(a))\}$.
    Chceme ukázať, že $S$ nie je splniteľná.
    Na základe 2. Herbrandovej vety stačí nájsť konečnú podmnožinu
    množiny základných inštancií klauzúl, ktorá nie je splniteľná.
    Takáto množina je napríklad $S' = \{ P(f(a)),\ \neg P(f(a))\}$.
\end{priklad}

\begin{priklad}
    Majme množinu klauzúl $S=\{\neg P(x) \lor Q(f(x),x),\
        P(g(b)),\ \neg Q(y,z) \}$.
    Táto množina nie je splniteľná -- vezmime napríklad
    \begin{equation*}
        S' = \{ \neg P(g(b)) \lor Q(f(g(b)), g(b)),\ P(g(b)),\ 
                \neg Q(f(g(b)), g(b)) \}
    \end{equation*}
\end{priklad}

\begin{priklad}
%%% {{{
    Uvažujme množinu klauzúl $S$:
    \begin{equation*}
    \begin{split}
        S = \big\{& \neg P(x,y,u) \lor \neg P(y,z,v) \lor 
                    \neg P(x,v,w) \lor P(u,z,w), \\
	         & \neg P(x,y,u) \lor \neg P(z,y,v) \lor
                    \neg P(u,z,w) \lor P(x,v,w), \\
	         & P(g(x,y),x,y), \\
                 & P(x,h(x,y),y), \\
                 & P(x,y,f(x,y), \\
                 & \neg P(k(v),x,k(x)) \\
                 & \big\}
    \end{split}
    \end{equation*}
    Chceme ukázať, že $S$ nie je splniteľná. Návod je napríklad
    takýto: Zostrojme si konečný uzavretý sémantický strom pre $S$
    a potom vypíšme základné inštancie klauzúl pripísaných jednotlivým
    cestám (vetvám) tohoto stromu.
    Možné riešenie je tak napríklad
    \begin{equation*}
    \begin{split}
        S' = \big\{& P(a,h(a,a),a), \\
                   & P(g(a,k(h(a,a))),a,k(h(a,a))),\\
                   & \neg P(k(h(a,a)),h(a,a),k(h(a,a))),\\
                   & \neg P(g(a,k(h(a,a))),a,k(h(a,a))) \lor
                    \neg P(a,h(a,a),a) \lor \\ & \phantom{\lor}
                    \neg P(g(a,k(h(a,a))),a,k(h(a,a))) \lor
                    P(k(h(a,a)),h(a,a),k(h(a,a))) \\
                &\big\}
    \end{split}
    \end{equation*}
%%% }}}
\end{priklad}

\begin{poznamka}[Gilmore, 1960]
    Nech $S_1',S_2',\dots$ sú možiny základných inštancií klauzúl z
    $S$. Gilmore vymyslel spôsob, ako generovať postupne
    $S_1',S_2',\dots$ a aj spôsob, ako overovať ich nesplniteľnosť.
    Problém bol, že algoritmické metódy na zisťovanie nesplniteľnosti
    pracovali iba pre menšie množiny klauzúl.
    $S_i'$ bola totiž konjunkcia základných inštancií klauzúl z $S$.
    Lenže $S$ je množina disjunkcií a dostaneme teda
    konjunktívnu normálnu formu. Túto formu bolo treba upraviť na
    disjunktívnu normálnu formu, pretože potom sa mohla optimalizovať
    metódami výrokovej logiky. Následne metóda vyhadzovala z DNF
    kontrárne dvojice.
    Pre veľa klauzúl krátkej dĺžky to znamenalo preberanie veľkého
    počtu možností.
    Ak máme $10$ klauzúl každá dĺžky 2 literály,
    potrebujeme preverovať $2^{10}$ prípadov -- zložitosť exponenciálne
    rastie.
\end{poznamka}

\begin{priklad}
    Majme množinu klauzúl $S=\{P(x),\ \neg P(a)\}$ a
    univerzum nech je $H_0 = \{a\}$.
    Ak zoberieme $S'=\{P(a), \neg P(a)\}$,
    máme $S_0' = P(a) \land \neg P(a)$, čo sa dá upraviť na $\eps$ a
    teda $S$ nie je splniteľná.
\end{priklad}


\begin{priklad}
    Majme $S=\{P(a),\ \neg P(x) \lor Q(f(x)),\ \neg Q(f(a)) \}$ a
    univerzum $H_0 = \{a\}$.
    \dots
    Dokázať nesplniteľnost množiny $S$ možno nasledovne:
    \begin{equation*}
    \begin{split}
        S_0' &=P(a)\land [\neg P(a)\lor Q(f(a))] \land \neg Q(f(a)) \\
             &=[P(a)\land \neg P(a) \land \neg Q(f(a))] \lor 
               [P(a) \land Q(f(a)) \land \neg Q(f(a))] \\
             &= \eps \lor \eps = \eps
    \end{split}
    \end{equation*}
\end{priklad}

\subsection{Dokazovacie pravidlá}

Zaviedli ich Martin Davis a Hilary Putnam ako súčasť ich algoritmu na
automatické dokazovanie formúl. Z pravidiel ktoré si uvedieme bude
najsilnejšie takzvané pravidlo rezu, pomocou ktorého sa dajú simulovať
aj ostatné pravidlá.

\subsubsection{Pravidlo tautológie} 
Nech $S$ je množina klauzúl.
Vynechajme z $S$ všetky tautologické klauzuly.
Množina $S'$, ktorá nám zostane, nie je splniteľná práve vtedy,
keď $S$ nie je splniteľná.

\begin{dokaz}
    Keď $S$ nie je splniteľné, tak ani $S'$ nie je splniteľné --
    tautológie sú splnené pre ľubovoľné interpretácie.
    To, čo zostane, hovorí, či množina je alebo nie je splniteľná.
    \\
\end{dokaz}

\subsubsection{Pravidlo jednoliterálnych klauzúl}
Nech $S$ je množina klauzúl a $L$ je nejaká jednoliterálová klauzula.
Vynechajme z $S$ všetky klauzuly, ktoré obsahujú literál $L$.
Nech $S'$ sú klauzuly, ktoré nám zostanú po vynechaní.
Môžu nastať dva prípady:
\begin{enumerate}
    \item $S' = \emptyset$. Potom množina klauzúl $S$ je splniteľná --
        stačí zobrať model, ktorý obsahuje $L$.

    \item $S' \neq \emptyset$. Vezmem si literál $\neg L$ a vynechám
        ho z z každej klauzuly, ktorá ho obsahuje.%
        \footnote{Pozor, prechod od $S$ k $S'$ je principiálny iný ako
            prechod od $S'$ ku $S''$. Prvý krát totiž mažeme celé
            klauzuly, zatiaľ čo druhýkrát iba literály v klauzulách.}
        Dostanem tak množinu klauzúl $S''$.
        Ak sa $\neg L$ nachádza v $S'$, po vynechaní
        $\neg L$ dostaneme $\eps$.
        Tvrdíme, že $S''$ nie je splniteľná
        $\iff$ $S$ nie je splniteľná.
\end{enumerate}

\begin{dokaz}
%%% {{{
    Máme $S'$, ktoré vzniklo vynechaním klauzúl obsahujúcich $L$ z $S$.
    Ak $S'=\emptyset$, každá klauzula z $S$ obsahuje $L$ v disjunkcii
    (špeciálne $L$ je tvaru $L \lor \eps$).
    Stačí nám ohodnotenie, kedy $L$ je pravdivé, čo zabezpečí
    pravdivosť celého výroku. 

    Keď $S'$ nie je prázdna, vytvoríme $S''$.
    Ideme ukázať, že $S''$ nie je splniteľná práve vtedy,
    keď $S$ nie je splniteľná.

    \begin{itemize}
    \item[$\Rightarrow:$] Budeme dokazovať sporom.
        Predpokladajme, že $S''$ nie je splniteľná a $S$ je splniteľná.
        Model existuje model $\mathcal{M}$ a tento musí obsahovať $L$.
        Lenže tým pádom v množine klauzúl $S''$ sú zbytky po vyhodení
        $\neg L$ splnené $\then$ $S''$ je splniteľná -- spor.

    \item[$\Leftarrow:$] Opačnú implikáciu budeme opäť dokazovať sporom.
        Nech $S''$ je splniteľná. Potom existuje model
        $\mathcal{M}''$ pre $S''$. Ak tomuto modelu pridám $L$, potom
        $\mathcal{M}'' \cup L$ je model pre $S$, čo je spor.
    \end{itemize}
%% }}}    
\end{dokaz}
\subsubsection{Pravidlo čistých literálov}

\begin{definicia}[Čistý literál]
    Literál $L$ základnej klauzuly z $S$ budeme nazývať čistým,
    ak sa literál $\neg L$ nevyskytuje v žiadnej základnej klauzule $S$.
\end{definicia}

\noindent
Teraz môžeme sformulovať pravidlo: \\
Vezmime si z $S$ literál $L$, ktorý je čistý
a vynechajme z $S$ všetky základné inštancie klauzúl obsahujúce $L$.
Množinu, ktorá nám ostala označme ako $S'$.
Tvrdíme, že $S$ nie je splniteľná $\iff$ $S'$ nie je splniteľná.


\begin{dokaz}
%%% {{{
    $S$ nie je splniteľná $\iff$ $S'$ nie je splniteľná.
    \begin{itemize}
    \item[$\Rightarrow:$] Budeme dokazovať sporom.
        Predpokladajme, že $S$ nie je splniteľná.
        ale $S'$ splniteľná je. Potom musí mať
        model $\mathcal{M}'$, ktorý jej vyhovuje a neobsahuje
        $L, \neg L$.  Keď si vytvorím model $\mathcal{M}=\mathcal{M}'\cup L$,
        potom $\mathcal{M}$ je modelom pre $S$. Čiže
        $S$ je splniteľná a to je spor.

    \item[$\Leftarrow:$] Predpokladajme, že
        $S'$ nie je splniteľná. Platí $S' \subseteq S$ a teda
        triviálne nie je splniteľná ani $S$.
    \end{itemize}
%%% }}}    
\end{dokaz}

\subsubsection{Pravidlo rezu}
Predpokladame, že množinu $S$ vieme vyjadriť v tvare
\begin{equation*}
    (A_1 \lor L) \land \ldots \land (A_m \lor L) \quad \land \quad
    (B_1 \lor \neg L) \land \ldots \land (B_n \lor \neg L) 
    \quad \land \quad R
\end{equation*}
pričom $A_i, B_i, R$ neobsahujú $L$ ani $\neg L$.
Označme si množiny
\begin{align*}
    S_1 &= A_1 \land A_2 \land \ldots \land A_m \land R \\
    S_2 &= B_1 \land B_2 \land \ldots \land B_n \land R
\end{align*}
Tieto množiny budeme tiež nazývať množiny rezu.
Tvrdíme, že $S$ nie je splniteľná $\iff$ $S_1 \lor S_2$ nie je
splniteteľná, čo je to isté ako že $S_1,S_2$ nie sú splniteľné.

\begin{dokaz}
    %%% {{{
    \noindent
    \begin{itemize}
    \item[$\Rightarrow:$] Dokazujme sporom.
        Nech $S_1 \lor S_2$ je splniteľná, 
        teda aspoň jeden člen disjunkcie je splniteľný.
        Bunv nech je splniteľná množina $S_1$. Teda, máme pre ňu model
        $\mathcal{M}_1$. Keď pridáme modelu $\mathcal{M}_1$ 
        klauzulu $\neg L$, dostávame model pre $S$.

    \item[$\Leftarrow:$] Pre spor predpokladajme, že $S$ je splniteľná.
        $S$ má tým pádom model, označme ho $\mathcal{M}$.
        Model $\mathcal{M}$ obsahuje buď $L$ alebo $\neg L$.
        Ak obsahuje $L$, $\mathcal{M}$ vyhovuje $S_2$. Naopak, ak
        obsahuje $\neg L$, model $\mathcal{M}$ vyhovuje
        $S_1$.\footnote{Na prednáške boli vymenené $S_1,S_2$. Som si
        však takmer istý, že správny dôkaz je tento.}
    \end{itemize}
    %%% }}}
\end{dokaz}

\begin{priklad}
    Majme množinu $S$ vyjadrenú v tvare
    $S=(P \lor Q \lor \neg R) \land (P \lor \neg Q) 
        \land \neg P \land R \land U$.
    Ukážeme, že množina klauzúl nie je splniteľná.

    \begin{itemize}
    \item $S=(P \lor Q \lor \neg R) \land (P \lor \neg Q) 
            \land \neg P \land R \land U$.

    \item $(Q \lor \neg R) \land  \neg Q \land R \land U$ -- použili
        sme pravidlo jednoliterálových klauzúl (PJK) pre $\neg P$.

    \item $\neg R \land R \land U$ -- použili
        sme PJK pre $\neg Q$.

    \item $\eps \land U$ -- použili
        sme PJK pre $R$. Je dôležité,
        že klauzulu $\neg R = \eps \lor \neg R$ 
        sme ale nemohli škrtnúť úplne, ostalo nám po nej $\eps$.

    \item $\eps \land \dots$ je vždy nesplniteľné a teda $S$ nie je
        splniteľná
    \end{itemize}
\end{priklad}

\begin{priklad}
    Uvažujme $S=(P \lor Q) \land \neg Q \land ( \neg P \lor Q \lor \neg R)$.
    Ukážte, že množina klauzúl $S$ je splniteľná.

    \begin{itemize}
    \item $S=(P \lor Q) \land \neg Q \land ( \neg P \lor Q \lor \neg R)$.
    \item $P \land (\neg P \lor \neg R)$ -- PJK pre $\neg Q$.
    \item $\neg R$ -- PJK pre $P$.
    \item Uvažujme interpretáciu $I=\{P,\neg Q,\neg R\}$. S je
        splniťeľná pri interpretácii $I$.
    \end{itemize}
\end{priklad}

\begin{priklad}
    Nech je $S=(P \lor Q) \land (P \lor \neg Q) \land
        (R \lor Q) \land (R \lor \neg Q)$.
    Ukážte, že $S$ je splniteľná.

    \begin{itemize}
    \item $S=(P \lor Q) \land (P \lor \neg Q) \land
            (R \lor Q) \land (R \lor \neg Q)$.
    
    \item $(R \lor Q) \land (R \lor \neg Q)$ -- pravidlo čistých
    literálov pre $P$

    \item $\neg \eps$ -- PČL pre $R$. Je dôležité si všimnúť, že nám
        ostalo splniteľné $\neg \eps$ a nie $\eps$.
    \item Pre interpretáciu $I=\{R,P\}$ je množina $S$ splnená.
    \end{itemize}
\end{priklad}

\begin{priklad}
    Uvažujme $S=(P \lor \neg Q) \land (\neg P \lor Q) \land 
                (Q \lor \neg R) \land (\neg Q \lor \neg R)$.
    Zistite, či množina je alebo nie je splniteľná.

    \begin{itemize}
    \item vytvoríme si množiny podľa pravidla rezu:
        \begin{align*}
            (P\land \neg Q) \land (Q \lor \neg R)  \land 
            (\neg Q \lor \neg R) \\
            (\neg P \lor Q) \land (Q \lor \neg R) \land 
            (\neg Q \lor \neg R)
        \end{align*}
        A dostávame množiny rezu
        \begin{align*}
            S_1 &= \neg Q \land (Q \lor \neg R) \land 
                (\neg Q \lor \neg R)\\
            S_2 &= Q \land (Q \lor \neg R) \land 
                (\neg Q \lor \neg R)
        \end{align*}

    \item Na množinu $S_1$ použijeme PJK s literálom $\neg Q$ a
        dostávame $\neg R \land \neg R$.
    \item Podobne, ak na množinu $S_2$ použijeme PJK s $Q$, opäť
        dostávame $\neg R \land \neg R$.
    \item $\neg R \land \neg R$ je splniteľná a preto je celá
        množina $S$ splniteľná.
    \end{itemize}
\end{priklad}

\begin{priklad}
    Majme $S=(P \lor Q) \land (P \lor \neg Q) \land 
        (R \lor Q) \land (R \lor \neg Q)$. 
    
    \begin{itemize}
    \item $P$ je čistý literál, použijeme PČL:
        $(R \lor Q) \land (R \lor \neg Q)$.
    \item $R$ je čistý literál a dostávame prázdny splniteľný výraz 
        $\neg \eps$
    \end{itemize}
\end{priklad}
